;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "iFlip.lisp")
(require "iimage.lisp")

(module mFlip
  (include-book "avl-rational-keys" :dir :teachpacks)
  (import IImage)
  
  (defun reverse-tree(image n)
    (if (empty-tree? image)
        (empty-tree)
        (tree (- (1+ n) (key image)) (data image) (reverse-tree (right image) n ) (reverse-tree (left image) n ))))
  
  (defun flip(image)
    (let* ((n (len (keys image))))
      (reverse-tree image n)))
  
  (defun flip-v(image)
    (let* ((header (cdr (avl-retrieve image -1)))
           (width (getWidth image))
           (height (getHeight image)))
      (avl-insert (avl-insert (avl-insert (flip (avl-delete (avl-delete (avl-delete image -1) -2) -3)) -1 header) -2 width) -3 height)))
  
  (defun flip-h-helper (image)
    (if (empty-tree? image)
        (empty-tree)
        (tree (key image) (flip (data image)) (flip-h-helper (left image)) (flip-h-helper (right image)))))
  
  (defun flip-h(image)
    (let* ((header (cdr (avl-retrieve image -1)))
           (width (getWidth image))
           (height (getHeight image)))
      (avl-insert (avl-insert (avl-insert (flip-h-helper (avl-delete (avl-delete (avl-delete image -1) -2) -3)) -1 header) -2 width) -3 height)))
  
  (defun MainFlip (tree args)
    (if (not (or (string-equal (car args) "V") (string-equal (car args) "H")))
        (mv tree (list "Invalid Argument - V or H expected"))
        (cond
          ((string-equal (car args) "V") (mv (flip-v tree) (list "Successfully flipped image vertically.")))
          ((string-equal (car args) "H") (mv (flip-h tree) (list "Successfully flipped image horizontally."))))))
        
  
  (export iFlip))